package cnf;

import java.util.HashSet;
import java.util.Set;

import java.util.HashMap;

import org.sat4j.core.VecInt;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.ISolver;

import data.Constant;
import file.FormGenerator;

public class Rules {

	private ISolver solver;
	private FormGenerator fg;

	public static final int RMAX = 9;
	public static final int RMIN = 0;
	public static final int CMAX = 9;
	public static final int CMIN = 0;
	public static final int VMAX = 7;
	public static final int VMIN = 1;
	
	private Set<Integer> destroyer;
	private Set<Integer> cruiser;
	private Set<Integer> battleship;
	private Set<Integer> submarine;
	

	private HashMap<Integer, Integer> sMap;

	public Rules(ISolver solver, FormGenerator fg) {
		this.solver = solver;
		this.fg = fg;
		this.destroyer = new HashSet<Integer>();
		this.cruiser = new HashSet<Integer>();
		this.battleship = new HashSet<Integer>();
		this.submarine = new HashSet<Integer>();
	}

	public Rules() {
		this.destroyer = new HashSet<Integer>();
		this.cruiser = new HashSet<Integer>();
		this.battleship = new HashSet<Integer>();
		this.submarine = new HashSet<Integer>();
	}
	
	public void setup() {
		int[] clause;
		try {
			// Definedness
			clause = new int[VMAX];
			for (int r = RMIN; r <= RMAX; r++) {
				for (int c = CMIN; c <= CMAX; c++) {
					for (int v = VMIN; v <= VMAX; v++) {
						clause[v - 1] = r * 100 + c * 10 + v;
					}
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);
				}
			}

			// Uniqueness
			clause = new int[2];
			for (int r = RMIN; r <= RMAX; r++) {
				for (int c = CMIN; c <= CMAX; c++) {
					for (int v = VMIN; v <= VMAX - 1; v++) {
						for (int t = v + 1; t <= VMAX; t++) {
							clause[0] = 0 - (r * 100 + c * 10 + v);// if cell
																	// has v
							clause[1] = 0 - (r * 100 + c * 10 + t);// then it
																	// can not
																	// have t
							solver.addClause(new VecInt(clause));
							fg.addClause(clause);
						}
					}
				}
			}

			// Diagonals
			clause = new int[2];
			for (int r = RMIN; r <= RMAX - 1; r++) {
				for (int c = CMIN; c <= CMAX - 1; c++) {
					clause[0] = r * 100 + c * 10 + Constant.WATER;// if not
																	// water
					clause[1] = (r + 1) * 100 + (c + 1) * 10 + Constant.WATER;// then
																				// diagonal
																				// is
																				// water
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);

				}
			}
			for (int r = RMAX; r >= RMIN - 1; r--) {
				for (int c = CMAX - 1; c >= CMIN; c--) {
					clause[0] = r * 100 + c * 10 + Constant.WATER;// if not
																	// water
					clause[1] = (r - 1) * 100 + (c + 1) * 10 + Constant.WATER;// then
																				// diagonal
																				// is
																				// water
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);
				}
			}

			// Boundary Constraints
			clause = new int[1];
			// no middle at the corners
			clause[0] = 0 - (RMIN * 100 + CMIN * 10 + Constant.MIDDLE);
			solver.addClause(new VecInt(clause));
			fg.addClause(clause);
			clause[0] = 0 - (RMIN * 100 + CMAX * 10 + Constant.MIDDLE);
			solver.addClause(new VecInt(clause));
			fg.addClause(clause);
			clause[0] = 0 - (RMAX * 100 + CMIN * 10 + Constant.MIDDLE);
			solver.addClause(new VecInt(clause));
			fg.addClause(clause);
			clause[0] = 0 - (RMAX * 100 + CMAX * 10 + Constant.MIDDLE);
			solver.addClause(new VecInt(clause));
			fg.addClause(clause);
			// ///////////////
			clause = new int[2];
			// if the first row contains middle then the cell below should be
			// water
			for (int c = CMIN + 1; c + 1 <= CMAX; c++) {
				clause[0] = 0 - (RMIN * 100 + c * 10 + Constant.MIDDLE);
				clause[1] = (RMIN + 1) * 100 + c * 10 + Constant.WATER;
				solver.addClause(new VecInt(clause));
				fg.addClause(clause);
			}
			// if the last row contains middle then the cell above should be
			// water
			for (int c = CMIN + 1; c + 1 <= CMAX; c++) {
				clause[0] = 0 - (RMAX * 100 + c * 10 + Constant.MIDDLE);
				clause[1] = (RMAX - 1) * 100 + c * 10 + Constant.WATER;
				solver.addClause(new VecInt(clause));
				fg.addClause(clause);
			}
			// if the first col contains middle then the cell on the right
			// should be water
			for (int r = RMIN + 1; r + 1 <= RMAX; r++) {
				clause[0] = 0 - (r * 100 + CMIN * 10 + Constant.MIDDLE);
				clause[1] = r * 100 + (CMIN + 1) * 10 + Constant.WATER;
				solver.addClause(new VecInt(clause));
				fg.addClause(clause);
			}
			// if the last col contains middle then the cell on the left should
			// be water
			for (int r = RMIN + 1; r + 1 <= RMAX; r++) {
				clause[0] = 0 - (r * 100 + CMAX * 10 + Constant.MIDDLE);
				clause[1] = r * 100 + (CMAX - 1) * 10 + Constant.WATER;
				solver.addClause(new VecInt(clause));
				fg.addClause(clause);
			}
			// no bottom in the first row
			clause = new int[1];
			for (int c = CMIN; c <= CMAX; c++) {
				clause[0] = 0 - (RMIN * 100 + c * 10 + Constant.BOTTOM);
				solver.addClause(new VecInt(clause));
				fg.addClause(clause);
			}
			// no top in the last row
			for (int c = CMIN; c <= CMAX; c++) {
				clause[0] = 0 - (RMAX * 100 + c * 10 + Constant.TOP);
				solver.addClause(new VecInt(clause));
				fg.addClause(clause);
			}
			// no right in the first col
			for (int r = RMIN; r <= RMAX; r++) {
				clause[0] = 0 - (r * 100 + CMIN * 10 + Constant.RIGHT);
				solver.addClause(new VecInt(clause));
				fg.addClause(clause);
			}
			// no left in the last col
			for (int r = RMIN; r <= RMAX; r++) {
				clause[0] = 0 - (r * 100 + CMAX * 10 + Constant.LEFT);
				solver.addClause(new VecInt(clause));
				fg.addClause(clause);
			}

			// if a cell contains circle then the adjacent cells are water
			clause = new int[2];
			for (int r = RMIN; r <= RMAX; r++) {
				for (int c = CMIN; c <= CMAX; c++) {
					clause[0] = 0 - (r * 100 + c * 10 + Constant.CIRCLE);
					if (r - 1 >= RMIN) {
						clause[1] = (r - 1) * 100 + c * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
					if (r + 1 <= RMAX) {
						clause[1] = (r + 1) * 100 + c * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
					if (c - 1 >= CMIN) {
						clause[1] = r * 100 + (c - 1) * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
					if (c + 1 <= CMAX) {
						clause[1] = r * 100 + (c + 1) * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
					submarine.add(r * 100 + c * 10 + Constant.CIRCLE);
				}
			}

			// if a cell contains middle *m* then the adjacent cells
			// |-----|t,m,w|-----| 
			// |l,m,w|-*m*-|r,m,w| 
			// |-----|b,m,w|-----| 
			//
			// |-|1|-|
			// |3|-|4|
			// |-|2|-|
			// also considered the case that not all adjacent cells can be water
			int[] clause1;
			clause = new int[4];
			clause1 = new int[3];
			for (int r = RMIN; r <= RMAX; r++) {
				for (int c = CMIN; c <= CMAX; c++) {
					clause[0] = 0 - (r * 100 + c * 10 + Constant.MIDDLE);
					clause1[0] = 0 - (r * 100 + c * 10 + Constant.MIDDLE);
					if (r - 1 >= RMIN) {// 1
						clause[1] = (r - 1) * 100 + c * 10 + Constant.TOP;
						clause[2] = (r - 1) * 100 + c * 10 + Constant.MIDDLE;
						clause[3] = (r - 1) * 100 + c * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
						clause1[1] = 0 - ((r - 1) * 100 + c * 10 + Constant.WATER);
						if (c - 1 >= CMIN) {
							clause1[2] = 0 - (r * 100 + (c - 1) * 10 + Constant.WATER);
							solver.addClause(new VecInt(clause1));
							fg.addClause(clause1);
						}
						if (c + 1 <= CMAX) {
							clause1[2] = 0 - (r * 100 + (c + 1) * 10 + Constant.WATER);
							solver.addClause(new VecInt(clause1));
							fg.addClause(clause1);
						}
					}
					if (r + 1 <= RMAX) {// 2
						clause[1] = (r + 1) * 100 + c * 10 + Constant.BOTTOM;
						clause[2] = (r + 1) * 100 + c * 10 + Constant.MIDDLE;
						clause[3] = (r + 1) * 100 + c * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
						clause1[1] = 0 - ((r + 1) * 100 + c * 10 + Constant.WATER);
						if (c - 1 >= CMIN) {
							clause1[2] = 0 - (r * 100 + (c - 1) * 10 + Constant.WATER);
							solver.addClause(new VecInt(clause1));
							fg.addClause(clause1);
						}
						if (c + 1 <= CMAX) {
							clause1[2] = 0 - (r * 100 + (c + 1) * 10 + Constant.WATER);
							solver.addClause(new VecInt(clause1));
							fg.addClause(clause1);
						}
					}
					if (c - 1 >= CMIN) {// 3
						clause[1] = r * 100 + (c - 1) * 10 + Constant.LEFT;
						clause[2] = r * 100 + (c - 1) * 10 + Constant.MIDDLE;
						clause[3] = r * 100 + (c - 1) * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
						clause1[1] = 0 - (r * 100 + (c - 1) * 10 + Constant.WATER);
						if (r - 1 >= RMIN) {
							clause1[2] = 0 - ((r - 1) * 100 + c * 10 + Constant.WATER);
							solver.addClause(new VecInt(clause1));
							fg.addClause(clause1);
						}
						if (r + 1 <= RMAX) {
							clause1[2] = 0 - ((r + 1) * 100 + c * 10 + Constant.WATER);
							solver.addClause(new VecInt(clause1));
							fg.addClause(clause1);
						}
					}
					if (c + 1 <= CMAX) {// 4
						clause[1] = r * 100 + (c + 1) * 10 + Constant.RIGHT;
						clause[2] = r * 100 + (c + 1) * 10 + Constant.MIDDLE;
						clause[3] = r * 100 + (c + 1) * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
						clause1[1] = 0 - (r * 100 + (c + 1) * 10 + Constant.WATER);
						if (r - 1 >= RMIN) {
							clause1[2] = 0 - ((r - 1) * 100 + c * 10 + Constant.WATER);
							solver.addClause(new VecInt(clause1));
							fg.addClause(clause1);
						}
						if (r + 1 <= RMAX) {
							clause1[2] = 0 - ((r + 1) * 100 + c * 10 + Constant.WATER);
							solver.addClause(new VecInt(clause1));
							fg.addClause(clause1);
						}
					}
				}
			}

			// if the cell has top *t* then the adjacent cells are
			// |---|-w-|---| 
			// |-w-|*t*|-w-| 
			// |---|b,m|---| 
			//
			// |-|1|-|
			// |3|-|4|
			// |-|2|-|
			clause = new int[2];
			for (int r = RMIN; r <= RMAX; r++) {
				for (int c = CMIN; c <= CMAX; c++) {
					clause[0] = 0 - (r * 100 + c * 10 + Constant.TOP);
					if (r - 1 >= RMIN) {// 1
						clause[1] = (r - 1) * 100 + c * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
					if (r + 1 <= RMAX) {// 2
						clause1 = new int[3];
						clause1[0] = 0 - (r * 100 + c * 10 + Constant.TOP);
						clause1[1] = (r + 1) * 100 + c * 10 + Constant.BOTTOM;
						clause1[2] = (r + 1) * 100 + c * 10 + Constant.MIDDLE;
						solver.addClause(new VecInt(clause1));
						fg.addClause(clause1);
					}
					if (c - 1 >= CMIN) {// 3
						clause[1] = r * 100 + (c - 1) * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
					if (c + 1 <= CMAX) {// 4
						clause[1] = r * 100 + (c + 1) * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
				}
			}

			// if the cell has bottom *b* then the adjacent cells are
			// |---|t,m|---| 
			// |-w-|*b*|-w-| 
			// |---|-w-|---| 
			//
			// |-|1|-|
			// |3|-|4|
			// |-|2|-|
			clause = new int[2];
			for (int r = RMIN; r <= RMAX; r++) {
				for (int c = CMIN; c <= CMAX; c++) {
					clause[0] = 0 - (r * 100 + c * 10 + Constant.BOTTOM);
					if (r - 1 >= RMIN) {// 1
						clause1 = new int[3];
						clause1[0] = 0 - (r * 100 + c * 10 + Constant.BOTTOM);
						clause1[1] = (r - 1) * 100 + c * 10 + Constant.TOP;
						clause1[2] = (r - 1) * 100 + c * 10 + Constant.MIDDLE;
						solver.addClause(new VecInt(clause1));
						fg.addClause(clause1);
					}
					if (r + 1 <= RMAX) {// 2
						clause[1] = (r + 1) * 100 + c * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
					if (c - 1 >= CMIN) {// 3
						clause[1] = r * 100 + (c - 1) * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
					if (c + 1 <= CMAX) {// 4
						clause[1] = r * 100 + (c + 1) * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
				}
			}

			// if the cell has left *l* then the adjacent cells are
			// |---|-w-|---| 
			// |-w-|*l*|r,m| 
			// |---|-w-|---| 
			//
			// |-|1|-|
			// |3|-|4|
			// |-|2|-|
			clause = new int[2];
			for (int r = RMIN; r <= RMAX; r++) {
				for (int c = CMIN; c <= CMAX; c++) {
					clause[0] = 0 - (r * 100 + c * 10 + Constant.LEFT);
					if (r - 1 >= RMIN) {// 1
						clause[1] = (r - 1) * 100 + c * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
					if (r + 1 <= RMAX) {// 2
						clause[1] = (r + 1) * 100 + c * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
					if (c - 1 >= CMIN) {// 3
						clause[1] = r * 100 + (c - 1) * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
					if (c + 1 <= CMAX) {// 4
						clause1 = new int[3];
						clause1[0] = 0 - (r * 100 + c * 10 + Constant.LEFT);
						clause1[1] = r * 100 + (c + 1) * 10 + Constant.RIGHT;
						clause1[2] = r * 100 + (c + 1) * 10 + Constant.MIDDLE;
						solver.addClause(new VecInt(clause1));
						fg.addClause(clause1);
					}
				}
			}

			// if the cell has right *r* then the adjacent cells are
			// |---|-w-|---|
			// |l,m|*r*|-w-|
			// |---|-w-|---|
			//
			// |-|1|-|
			// |3|-|4|
			// |-|2|-|
			clause = new int[2];
			for (int r = RMIN; r <= RMAX; r++) {
				for (int c = CMIN; c <= CMAX; c++) {
					clause[0] = 0 - (r * 100 + c * 10 + Constant.RIGHT);
					if (r - 1 >= RMIN) {// 1
						clause[1] = (r - 1) * 100 + c * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
					if (r + 1 <= RMAX) {// 2
						clause[1] = (r + 1) * 100 + c * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
					if (c - 1 >= CMIN) {// 3
						clause1 = new int[3];
						clause1[0] = 0 - (r * 100 + c * 10 + Constant.RIGHT);
						clause1[1] = r * 100 + (c - 1) * 10 + Constant.LEFT;
						clause1[2] = r * 100 + (c - 1) * 10 + Constant.MIDDLE;
						solver.addClause(new VecInt(clause1));
						fg.addClause(clause1);
					}
					if (c + 1 <= CMAX) {// 4
						clause[1] = r * 100 + (c + 1) * 10 + Constant.WATER;
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
				}
			}

			// 3 middles can not be adjacents
			// horizontially
			clause = new int[3];
			for (int r = RMIN; r <= RMAX; r++) {
				for (int c = CMIN; c + 2 <= CMAX; c++) {
					clause[0] = 0 - (r * 100 + c * 10 + Constant.MIDDLE);
					clause[1] = 0 - (r * 100 + (c + 1) * 10 + Constant.MIDDLE);
					clause[2] = 0 - (r * 100 + (c + 2) * 10 + Constant.MIDDLE);
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);
				}
			}
			// vertically
			for (int r = RMIN; r + 2 <= RMAX; r++) {
				for (int c = CMIN; c <= CMAX; c++) {
					clause[0] = 0 - (r * 100 + c * 10 + Constant.MIDDLE);
					clause[1] = 0 - ((r + 1) * 100 + c * 10 + Constant.MIDDLE);
					clause[2] = 0 - ((r + 2) * 100 + c * 10 + Constant.MIDDLE);
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);
				}
			}

			//aux variable constraint
			//destroyer (2 cells)
			clause = new int[3];
			//horizontal destroyer
			for (int r = RMIN; r <= RMAX; r++) {
				for (int c = CMIN; c+1 <= CMAX; c++) {
					clause[0] = 0 - (r*100 + c*10 + Constant.LEFT);
					clause[1] = 0 - (r*100 + (c+1)*10 + Constant.RIGHT);
					clause[2] = r*100 + (c+1)*10 + Constant.DESTROYER;
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);
					destroyer.add(clause[2]);
				}
			}
			//vertical destroyer
			for (int r = RMIN; r+1 <= RMAX; r++) {
				for (int c = CMIN; c <= CMAX; c++) {
					clause[0] = 0 - (r*100 + c*10 + Constant.TOP);
					clause[1] = 0 - ((r+1)*100 + c*10 + Constant.BOTTOM);
					clause[2] = (r+1)*100 + c*10 + Constant.DESTROYER;
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);
					destroyer.add(clause[2]);
				}
			}
			
			//cruiser (3 cell)
			clause = new int[4];
			//horizontal cruiser
			for (int r = RMIN; r <= RMAX; r++) {
				for (int c = CMIN; c+2 <= CMAX; c++) {
					clause[0] = 0 - (r*100 + c*10 + Constant.LEFT);
					clause[1] = 0 - (r*100 + (c+1)*10 + Constant.MIDDLE);
					clause[2] = 0 - (r*100 + (c+2)*10 + Constant.RIGHT);
					clause[3] = r*100 + (c+2)*10 + Constant.CRUISER;
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);
					cruiser.add(clause[3]);
				}
			}
			//vertical cruiser
			for (int r = RMIN; r+2 <= RMAX; r++) {
				for (int c = CMIN; c <= CMAX; c++) {
					clause[0] = 0 - (r*100 + c*10 + Constant.TOP);
					clause[1] = 0 - ((r+1)*100 + c*10 + Constant.MIDDLE);
					clause[2] = 0 - ((r+2)*100 + c*10 + Constant.BOTTOM);
					clause[3] = (r+2)*100 + c*10 + Constant.CRUISER;
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);
					cruiser.add(clause[3]);
				}
			}
			
			//battleship (4 cell)
			clause = new int[5];
			//horizontal battleship
			for (int r = RMIN; r <= RMAX; r++) {
				for (int c = CMIN; c+3 <= CMAX; c++) {
					clause[0] = 0 - (r*100 + c*10 + Constant.LEFT);
					clause[1] = 0 - (r*100 + (c+1)*10 + Constant.MIDDLE);
					clause[2] = 0 - (r*100 + (c+2)*10 + Constant.MIDDLE);
					clause[3] = 0 - (r*100 + (c+3)*10 + Constant.RIGHT);
					clause[4] = r*100 + (c+3)*10 + Constant.BATTLESHIP;
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);
					battleship.add(clause[4]);
				}
			}
			//vertical battleship
			for (int r = RMIN; r+3 <= RMAX; r++) {
				for (int c = CMIN; c <= CMAX; c++) {
					clause[0] = 0 - (r*100 + c*10 + Constant.TOP);
					clause[1] = 0 - ((r+1)*100 + c*10 + Constant.MIDDLE);
					clause[2] = 0 - ((r+2)*100 + c*10 + Constant.MIDDLE);
					clause[3] = 0 - ((r+3)*100 + c*10 + Constant.BOTTOM);
					clause[4] = (r+3)*100 + c*10 + Constant.BATTLESHIP;
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);
					battleship.add(clause[4]);
				}
			}
			
			// variables needed for counting
			int n;
			int k;
			Integer[] aux;
			
			for (int loop = 1; loop <= 4; loop++) {
				switch (loop) {
				case 1:
					// count the destroyers
					aux = destroyer.toArray(new Integer[destroyer.size()]);
					// number of destroyers <= 3, here X = aux
					k = 3;
					break;
				case 2:
					// count the cruisers
					aux = cruiser.toArray(new Integer[cruiser.size()]);
					// number of cruisers <= 2, here X = aux
					k = 2;
					break;
				case 3:
					// count the battleships
					aux = battleship.toArray(new Integer[battleship.size()]);
					n = aux.length;
					// number of battleships <= 1, here X = aux
					k = 1;
					break;
				default:
					aux = submarine.toArray(new Integer[submarine.size()]);
					k = 4;
					break;
				}
				
				n = aux.length;
				newS();

				// ~X1 | S11
				clause = new int[2];
				clause[0] = 0 - aux[0];
				clause[1] = getS(1, 1);
				solver.addClause(new VecInt(clause));
				fg.addClause(clause);

				// ~Xn | ~S(n-1)k
				clause = new int[2];
				clause[0] = 0 - aux[n - 1];
				clause[1] = 0 - getS(n - 1, k);
				solver.addClause(new VecInt(clause));
				fg.addClause(clause);

				// ~S1j
				// j in (1, k]
				clause = new int[1];
				for (int j = 2; j <= k; j++) {
					clause[0] = 0 - getS(1, j);
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);
				}

				for (int i = 2; i < n; i++) {
					clause = new int[2];
					// ~Xi | Si1
					// i in (1, n)
					clause[0] = 0 - aux[i - 1];
					clause[1] = getS(i, 1);
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);

					// ~S(i-1)1 | Si1
					// i in (1, n)
					clause[0] = 0 - getS(i - 1, 1);
					clause[1] = getS(i, 1);
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);

					// ~Xi | ~S(i-1)k
					// i in (1, n)
					clause[0] = 0 - aux[i - 1];
					clause[1] = 0 - getS(i - 1, k);
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);

					for (int j = 2; j <= k; j++) {
						// ~Xi | ~S(i-1)(j-1) | Sij
						// i in (1, n)
						// j in (1, k]
						clause = new int[3];
						clause[0] = 0 - aux[i - 1];
						clause[1] = 0 - getS(i - 1, j - 1);
						clause[2] = getS(i, j);
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);

						// ~S(i-1)j | Sij
						clause = new int[2];
						clause[0] = 0 - getS(i - 1, j);
						clause[1] = getS(i, j);
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
				}

				// number of ~ship <= n - k, here X = ~aux
				k = n - k;
				newS();

				// ~X1 | S11
				clause = new int[2];
				clause[0] = aux[0];
				clause[1] = getS(1, 1);
				solver.addClause(new VecInt(clause));
				fg.addClause(clause);

				// ~Xn | ~S(n-1)k
				clause = new int[2];
				clause[0] = aux[n - 1];
				clause[1] = 0 - getS(n - 1, k);
				solver.addClause(new VecInt(clause));
				fg.addClause(clause);

				// ~S1j
				// j in (1, k]
				clause = new int[1];
				for (int j = 2; j <= k; j++) {
					clause[0] = 0 - getS(1, j);
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);
				}

				for (int i = 2; i < n; i++) {
					clause = new int[2];
					// ~Xi | Si1
					// i in (1, n)
					clause[0] = aux[i - 1];
					clause[1] = getS(i, 1);
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);

					// ~S(i-1)1 | Si1
					// i in (1, n)
					clause[0] = 0 - getS(i - 1, 1);
					clause[1] = getS(i, 1);
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);

					// ~Xi | ~S(i-1)k
					// i in (1, n)
					clause[0] = aux[i - 1];
					clause[1] = 0 - getS(i - 1, k);
					solver.addClause(new VecInt(clause));
					fg.addClause(clause);

					for (int j = 2; j <= k; j++) {
						// ~Xi | ~S(i-1)(j-1) | Sij
						// i in (1, n)
						// j in (1, k]
						clause = new int[3];
						clause[0] = aux[i - 1];
						clause[1] = 0 - getS(i - 1, j - 1);
						clause[2] = getS(i, j);
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);

						// ~S(i-1)j | Sij
						clause = new int[2];
						clause[0] = 0 - getS(i - 1, j);
						clause[1] = getS(i, j);
						solver.addClause(new VecInt(clause));
						fg.addClause(clause);
					}
				}
			}

		} catch (ContradictionException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
	}

	/**
	 * Gets the s.
	 * 
	 * @param i
	 *            the i
	 * @param j
	 *            the j
	 * @return the s
	 */
	private int getS(int i, int j) {
		// return sS + i * k + (j - 1);
		int key = i * 100 + j;
		if (sMap.containsKey(key)) {
			return sMap.get(key);
		} else {
			sMap.put(key, Hints.sS);
			return Hints.sS++;
		}
	}

	/**
	 * New s.
	 * 
	 * @param n
	 *            the n
	 * @param k
	 *            the k
	 */
	private void newS() {
		if (Hints.sS == 0) {
			Hints.sS = 1001;
		}
		sMap = new HashMap<Integer, Integer>();
	}
	
}
